i:Id, L:(Knd List), l:IdLnk, tg:Id.
@i: only L sends on (l with tg) 
realizes es.
e:E. (loc(e) = i  Id)  ((null(sends(l,tg,e))))  (kind(e)  L) 

latex

Definitions	t  T, x:A. B(x)
Lemmas	not wf, assert wf, null wf3